λ cube
ラムダ・キューブ - Wikipedia
Lambda cube - Wikipedia
λ計算
ラムダ計算 - Wikipedia
單純型附きλ計算 (simply-typed lambda calculus)$ \lambda\to
項に依存した項。一階命題論理
型付きラムダ計算 - Wikipedia
Typed lambda calculus - Wikipedia
lambda-calculus in nLab
三軸
多相型 (polymorphism)$ \lambda 2
型に依存した項。二階命題論理
ポリモーフィズム - Wikipedia
polymorphism in nLab
parametric 多相
System F
System F - Wikipedia
型演算 (type operators)$ \lambda\underline\omega
型に依存した型。弱性高階命題論理
代數的 data 型 (ADT)
依存型 (dependent type)$ \lambda\Pi
項に依存した型。一階述語論理 (FOL)
依存型 - Wikipedia
Dependent type - Wikipedia
三軸全てを備へた calculus of constructions (CoC)$ \lambda C
Calculus of constructions - Wikipedia
calculus of constructions in nLab
高階述語論理